\begin{tabbing}
d{-}world{-}state($D$;$i$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=:M($i$).(timed)state\+
\\[0ex]$\times$ (:Action(d{-}decl($D$;$i$))
\\[0ex]$\times$ (\{$m$:M($i$).Msg$\mid$ source(mlnk($m$)) = $i$\}  List))
\-
\end{tabbing}